Use E-matching on index expressions to instantiate quantifiers when
eager instantiation (aka enumerative instantiation) cannot be applied.

Replace the simplistic E-matching in instantiate_one_quantifier with a
complete instantiation approach based on:

  Yeting Ge and Leonardo de Moura, "Complete instantiation for quantified
  formulas in Satisfiability Modulo Theories", CAV 2009.

The paper shows that for essentially uninterpreted formulas (where
quantified variables only appear as arguments of uninterpreted functions),
the quantifier can be eliminated by instantiating with a finite set of
ground terms computed as the least fixed point of a system of set
constraints (ΔF). In CBMC's context, array accesses (index_exprt) play
the role of uninterpreted functions.

Key changes:

- find_index_contexts: Properly decomposes array index expressions into
  bound_var + offset form using pre-order traversal. Handles patterns
  var, cast(var), var+r, r+var, var-r. This implements the offset
  extension from Section 4 of the paper, where for f(x_i + r) we
  generate constraints S_{k,i} + r ⊆ A_{f,j} and A_{f,j} - r ⊆ S_{k,i}.

- collect_ground_indices: Collects ground index terms from both
  index_exprt (array reads) and with_exprt (array writes) in the
  bitvector cache, seeding the sets A_{f,j} from the paper.

- compute_instantiation_set: Computes the least fixed point of the set
  constraint system ΔF. Uses integer arithmetic when all offsets and
  ground indices are numeric constants (avoiding expression growth), with
  a symbolic fallback using simplify_expr. Bounded by max_iterations and
  max_terms to handle non-stratified (non-FEU) cases.

- arrays_match: SSA-aware array comparison using L1 object identifiers
  to match across SSA versions. For nested array accesses (e.g.,
  multi-dimensional arrays like a[i][j]), recursively matches the base
  array and compares simplified indices, since the pattern may contain
  unsimplified arithmetic (e.g., cast(0 % 2)) that is semantically
  equal to a constant in the cache.

Instantiation terms are sorted (via irept::operator<) before generating
the conjunction/disjunction to ensure deterministic SAT clause ordering.
Without this, MiniSat performance varies from sub-second to minutes on
the same UNSAT instance depending on hash-dependent iteration order,
which changes with file paths embedded in source locations.

This enables verification of properties that depend on relationships
between adjacent array elements, such as:
  forall j: arr[j+1] == arr[j] + 1
which the previous E-matching could not handle because it did not
generate the ground terms needed for the offset positions.

Add two regression tests exercising the complete instantiation approach:

- Quantifiers-offset-instantiation: Tests the offset pattern arr[j+1]
  from Section 4 of Ge & de Moura (2009). The quantifier
    forall j < n-1: arr[j+1] == arr[j] + 1
  requires the set constraint fixed-point to generate ground terms for
  both arr[j] and arr[j+1] positions. Without the offset handling, the
  instantiation misses the terms needed to chain the equalities.

- Quantifiers-fixpoint-instantiation: Tests that the fixed-point
  computation correctly propagates through multiple iterations. The
  property arr[2] > 0 requires two steps of reasoning:
    j=0: arr[0]>0 => arr[1]>0
    j=1: arr[1]>0 => arr[2]>0
  This exercises the iterative nature of the ΔF fixed-point from
  Section 3 of the paper, where instantiating with one set of terms
  generates new ground terms that feed back into the next iteration.

Add a -t <secs> option (and TESTPL_TIMEOUT environment variable) to
test.pl for enforcing a wall-clock timeout on each individual test.

The implementation replaces the system() call in run() with fork/exec,
placing the child in its own process group (setpgrp). When the timeout
fires via Perl's alarm(), the entire process group is killed with
SIGKILL, ensuring all child processes (bash, cbmc, solvers) are cleaned
up. On timeout the test is marked as failed and a synthetic output file
is written so that the pattern-matching logic does not crash.

The timeout defaults to 0 (disabled), preserving existing behaviour
unless -t is explicitly passed or TESTPL_TIMEOUT is set.